\begin{tabbing}
$\forall$\=$E$:Type, ${\it eq}$:EqDecider($E$), $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), ${\it loc}$:($E$$\rightarrow$Id),\+
\\[0ex]$k$:($E$$\rightarrow$Knd), $v$:($e$:$E$$\rightarrow$eventtype($k$;${\it loc}$;$V$;$M$;$e$)), $w$, $a$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$)),
\\[0ex]${\it snds}$:($l$:IdLnk$\rightarrow$$E$$\rightarrow$(Msg\_sub($l$;$M$) List)), ${\it sndr}$:(\{$e$:$E$$\mid$ isrcv($k$($e$)) \}$\rightarrow$$E$),
\\[0ex]$i$:($e$:\{$e$:$E$$\mid$ isrcv($k$($e$)) \}$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it snds}$(lnk($k$($e$)),${\it sndr}$($e$))$\parallel$}}$), $f$:($E$$\rightarrow\mathbb{B}$),
\\[0ex]${\it prd}$:(\{${\it e'}$:$E$$\mid$ $\neg$$f$(${\it e'}$) \}$\rightarrow$$E$), ${\it cl}$:($E$$\rightarrow$$E$$\rightarrow$Prop),
\\[0ex]$p$:ESAxioms(\=$E$;$T$;$M$;\+
\\[0ex]${\it loc}$;$k$;$v$;
\\[0ex]$w$;$a$;
\\[0ex]${\it snds}$;${\it sndr}$;$i$;
\\[0ex]$f$;${\it prd}$;
\\[0ex]${\it cl}$), $r$:ESAtomAxiom\{i:l\}($T$;$\lambda$$i$,$k$. kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )).
\-\-\\[0ex]mk{-}es0($E$;${\it eq}$;$T$;$V$;$M$;${\it loc}$;$k$;$v$;$w$;$a$;${\it snds}$;${\it sndr}$;$i$;$f$;${\it prd}$;${\it cl}$;$p$;$r$) $\in$ ES0
\end{tabbing}